Nuprl Lemma : qdot_wf
11,40
postcript
pdf
as
,
bs
:(
List). qdot(
as
;
bs
)
latex
Definitions
x
.
t
(
x
)
,
qdot(
as
;
bs
)
,
t
T
,
x
:
A
.
B
(
x
)
,
x
(
s
)
,
S
T
Lemmas
zip
wf
,
int
inc
rationals
,
pi2
wf
,
pi1
wf
,
qmul
wf
,
qadd
wf
,
rationals
wf
,
reduce
wf
origin
as, bs:(
List). qdot(as;bs) 
as, bs:( List). qdot(as;bs) 
x. t(x) Tx:A. B(x)
T